//MAX-SAT problem-depended class
//$Id: maxsat.h 175 2009-09-12 17:34:23Z Oleg.Bulychov $
#pragma once
#ifndef MAXSAT_H
#define MAXSAT_H

#include "src/heo/include/lf_endl.h"
#include "src/heo/include/random.h"
#include "src/heo/include/reflection.h"
#include "src/heo/include/optimization_direction.h"

struct MaxSat_Config
{
    double      initial_probability_;
    int         limit_output_;

    template<class V>
    void accept(V& v)
    {
        v(VAR_(initial_probability),        0.5);
        v(VAR_(limit_output),               20);
    }
};
//__________________________________________________________________________________
struct MaxSat_Problem
{
    int dimension_;
    int clause_count_;
    std::vector<int> data_;

    explicit MaxSat_Problem():
        dimension_(0)
    {}

    template<class I>
    bool read(I& in)
    {
        std::string s;
        in >> s;
        if (s != "p")
            return false;
        in >> s;
        if (s != "cnf")
            return false;
        in >> dimension_ >> clause_count_;
        if (dimension_ <= 0 || clause_count_ <= 0)
            return false;
        data_.reserve(3 * clause_count_);
        int k = 0;
        for (int i = 0; i < clause_count_; ++i)
        {
            int j = 0;
            size_t n = data_.size();
            data_.push_back(0);
            ++k;
            for (;; ++j, ++k)
            {
                int lit;
                in >> lit;
                if (!lit)
                    break;
                data_.push_back(lit);
            }
            if (j <= 0 || j > dimension_)
                return false;
            data_[n] = j;
        }
        return true;
    }
};
//__________________________________________________________________________________
//__________________________________________________________________________________
class MaxSat_Solution
{
    DISALLOW_COPY_AND_ASSIGN(MaxSat_Solution);
public:
    typedef maximization<> TDirection;
    typedef int            TCostType;
protected:
    bool*        data_;
    size_t       dim_;
    TCostType    cost_;
    bool         changed_;
public:
    explicit MaxSat_Solution(): data_(NULL), dim_(0), cost_(0), changed_(false)
    {}

    ~MaxSat_Solution()
    {
        delete[] data_;
    }

    void init(MaxSat_Problem const& problem, MaxSat_Config const& cfg)
    {
        dim_  = problem.dimension_;
        data_ = new bool[dim_];
    }

    void generate_Random(MaxSat_Config const& cfg, uniform_random& rnd)
    {
        for (size_t i = 0; i < dim_; ++i)
        {
            bool f = rnd.next_Double() < cfg.initial_probability_;
            data_[i] = f;
        }
        changed_ = true;
    }

    void generate_Trivial()
    {
        for (size_t i = 0; i < dim_; ++i)
        {
            data_[i] = false;
        }
        changed_ = false;
        cost_ = 0;
    }

    int get_Cost() const
    {
        ASSERT_(!changed_);
        return cost_;
    }

    void evaluate(MaxSat_Problem const& problem)
    {
        if (!changed_)
            return;
        changed_ = false;
        int f = 0;
        int const* clause = &problem.data_[0];
        for (int i = 0; i < problem.clause_count_; ++i)
        {
            int clause_length = *clause++;
            for (int j = 0; j < clause_length; ++j)
            {
                int lit = clause[j];
                if (lit < 0)
                {//!x 
                    if (!data_[-lit - 1])
                    {
                        ++f;
                        break;
                    }
                }
                else
                {//x
                    if (data_[lit - 1])
                    {
                        ++f;
                        break;
                    }
                }
            }
            clause += clause_length;
        }
        cost_ = f;
    }

    void assign(MaxSat_Solution const& sol)
    {
        ASSERT_(dim_);
        ASSERT_(dim_ == sol.dim_);
        size_t size = dim_;
        for (size_t i = 0; i < size; ++i)
        {
            data_[i] = sol.data_[i];
        }
        changed_ = sol.changed_;
        cost_    = sol.cost_;
    }

    void print(std::ostream& os, MaxSat_Problem const& problem, MaxSat_Config const& cfg)
    {
        for (int i = 0; i < (int)dim_; ++i)
        {
            os << (data_[i] ? i + 1 : -i - 1) << " ";
            if (i > cfg.limit_output_)
            {
                os << "...";
                break;
            }
        }
        os << lf
            << "cost: " << get_Cost() << lf
            << "clauses: " << problem.clause_count_ << lf
            << "not satisfied: " << problem.clause_count_ - get_Cost() << lf;
    }

    bool is_Solved(MaxSat_Problem const& problem) const
    {
        return cost_ == problem.dimension_;
    }

    template<class V>
    void accept(V& v)
    {
        v(cost_);
        v(changed_);
        v(data_, 0, meta::ptr_size(dim_));
    }
};
//__________________________________________________________________________________

#endif
//EOF!
